k:Knd, f, g:Top. islocal(k)  (kindcase(k; a.f(a); l,t.g(l,t) ) ~ g(lnk(k),tag(k))) 

latex

Definitions	Knd, kindcase(k; a.f(a); l,t.g(l;t) ), b, islocal(k), act(k), lnk(k), tag(k), x(s), x(s1,s2), P  Q, False, A, x:A. B(x), True, t  T, Top
Lemmas	top wf, true wf, not wf, false wf, Knd wf